Inductive MatrixExp: Type :=
  | matrix_exp_init : ArithExp -> ArithExp -> MatrixExp
  | matrix_exp_lit  : forall A m n, Matrix A m n -> MatrixExp
  | matrix_exp_id   : Id -> MatrixExp
.